freenode_mathfandomcom-20200215-history
Functors and Natural Transformations
Topic Functors and natural transformations, Yoneda's Lemma, adjoints and structures arising from them were among the topics covered. Seminar 20:58:44 Jafet: _llll_, does this build on last week's? 20:58:57 _llll_: yeah, pretty much 21:00:06 ChanServ changed the topic of #mathematics to: Seminar in progress. If you want to ask a question, say ! and wait to be called 21:00:13 _llll_: OK, let's get going 21:00:27 kommodore: hurray! 21:00:29 _llll_: today's topic is functors, natural trnasofmrations and the yoneda lemma. 21:00:39 _llll_: monads may be mentioned if there is time at the end 21:01:03 _llll_: OK, so last time i defined category and said that pretty much everything forms a category 21:01:19 _llll_: so it's reasonable to assume that "categories" themselves form a category 21:01:35 _llll_: ie, given categories CC and DD there should be a notion of map F:CC-->DD 21:01:43 _llll_: such an F is called a "functor" 21:02:03 _llll_: the definition is what you'd expect, F sends an object A in CC to an object FA in DD 21:02:18 _llll_: and if f:A-->B is a map in CC, then it gets mapped to Ff:FA-->FB in DD 21:02:35 _llll_: and if g:B-->C is another map in CC then Ff # Fg = F(f#g) 21:02:58 _llll_: (so recall that im writing composition of f:A-->B followd by g:B-->C as f#g :A-->C 21:03:13 _llll_: the final condition is that F(id_A)=id_FA ie identities get apped to identities 21:03:55 _llll_: composing functors is just like composing functions, and there is an identity functor id_CC : CC-->CC which just sends an object to itself (and similarly on morphisms) 21:04:09 _llll_: so we get a category CAT where the objects are categories and the maps are functors 21:04:16 ness: ! 21:04:20 _llll_: go ahead ness 21:04:35 ness: are there functors between every two objects in CAT? 21:05:01 _llll_: not necessarily, CC can have no objects and no arrows (the empty category) 21:05:11 _llll_: so then there are no functors DD--> "the empty category" 21:05:21 ness: oh 21:05:37 ness: thanks 21:05:39 _llll_: but otherwise you can just pick X in DD and send every object to X and every map to the identity on X 21:06:13 _llll_: (oh, well, if DD is also "the empty category" then there is actually a map from "the empty category" to itself, namely the identity functor) 21:06:16 _llll_: but, anway 21:06:51 _llll_: examples of functors are sending a group G to the set of elements of G 21:07:16 _llll_: this is U:Grp --> Set the "forgetful functor" -- you forget that G is a group, ie UG is just a set 21:07:43 _llll_: going the other way, from a set X you can form the free group on X, this gives a functor F:Grp --> Set 21:08:06 _llll_: so now suppose that we have two functors F and G which both go CC-->DD 21:08:21 _llll_: we can define a map F-->G 21:08:30 _llll_: ie something that goes between *functors* 21:08:54 _llll_: this is called a "natural transformation" 21:09:14 _llll_: the definition is that m:F-->G means that for every X in CC we get a map m_X FX-->GX in DD 21:09:49 _llll_: such that whenever f:A-->B is a map in CC, m_A # Gf = Ff # m_B 21:10:03 _llll_: this equation is best pictured as a square, which i will now attempt to draw ,----[ a picture of what it means for m:F-->G (pasted to pastebin.ca during the seminar ] | Naturality condition | | | Let F and G be functors CC-->DD. | Then "m:F-->G is a natural transform" means that for all A in CC | | m(A) : FA-->GA in DD | | and for all f:A-->B in CC, | | FA --m(A)--> GA | | | | Ff| |Gf (1) "Naturality square for m at f" | | | | v v | FB --m(B)--> GB | | commutes, i.e., | | m(A) # Gf = Ff # m(B) (2) | | for all f:A-->B in CC | | Equvialently, let 1 be the poset {0<=1} considered as a category. | Then m is "the same" as a functor | m:CCx1 -->DD is | with | CC--i_0-->CCx1--m -->DD = F | CC--i_1-->CCx1--m -->DD = G | | where i_0(A)=(A,0) and i_1(A)=(A,1) -- ie a natural transformation is | a homotopy. | | Remark 1: There are functors Ner and |-| | Cat--(Ner)-->SSet--(|-|)-->Top | | which turn natural transformations into real homotopies. Here SSet is | the category of simplicial sets. | | Remark 2: The map equal to either side of equation (2) is the diagonal | of the square (1). We can write it as m^f : FA-->GB then we have | split the square into two triangles -- this is how homotopies of | simplicial sets work. ( m^f=m(f,0<=1) with the previous formulation) `---- 21:11:52 _llll_: so you can compose natural transforms in (hopefully) the obvious way 21:12:17 ~lxuser: ! 21:12:20 _llll_: so there is a category CC,DD where the objects are functors CC-->DD and the maps are natural transformations 21:12:23 _llll_: go ahead lxuser 21:13:06 ~lxuser: can you form functors between a category and itself? 21:13:36 _llll_: sure, F:CC-->CC is always possible, there is one fucntor called "the identity on CC" which sends A in CC to A 21:13:40 _llll_: and f:A-->B to f 21:14:18 _llll_: (a monad is a special kind of functor from a category to itself) 21:14:41 _llll_: so to illustrate natural transformations a bit more, im going to prove (a version of) "the yoneda lemma" 21:14:48 _llll_: this is about functors CC-->Set 21:15:15 _llll_: ie we fix a category CC and consider the category CC,Set of functors from CC to Set 21:15:37 _llll_: one example is the functor CC(A,-) 21:15:54 _llll_: this notation is meant to suggest that A is fixed in CC, and that - is a "placeholder" 21:16:00 _llll_: CC(A,-):CC-->Set 21:16:12 _llll_: it sends objects B in CC to the set CC(A,B) 21:16:21 _llll_: ie to the set of maps from A to B in CC. 21:16:43 _llll_: if f:B-->B' then CC(A,-) has to send f to a function from CC(A,B) to CC(A,B') 21:16:50 _llll_: which function should it be? 21:17:04 _llll_: the obvious way is to send g:A-->B to g#f 21:17:19 _llll_: (since g#f goes A-->B' this ends in the right place) 21:17:32 _llll_: it's easy to check that C(A,-) really is a functor 21:18:34 _llll_: The yoneda lemma says that if F:CC-->Set is any other functor, then there is a natural bijection between natural tramsformations CC(A,-) to F and the set FA 21:18:55 _llll_: it's actually really easy to prove, once you get the notation straight 21:19:02 _llll_: so what does F:CC-->Set look like? 21:19:15 _llll_: so if A is an object in CC, FA is some set 21:19:28 _llll_: and if f:A-->B then Ff is a function FA-->FB 21:19:37 thermoplyae: ! 21:19:42 _llll_: go ahead thermoplyae 21:19:47 thermoplyae: does the word 'natural' in 'natural bijection' have meaning? 21:19:54 _llll_: ah, yes 21:20:18 _llll_: it means that actually it is part of a natural transformation which is an isomorphism 21:20:32 _llll_: the bijection if CC,Set(CC(A,-),F) ~ FA 21:20:39 _llll_: and it is natural in both A and F 21:20:54 _llll_: so *actualyl* there are functors CC^op x CC,Set --> Set 21:21:02 _llll_: one sends (A,F) to CC,Set(CC(A,-),F) 21:21:08 _llll_: and the other sends (A,F) to FA 21:21:27 _llll_: and these two are naturally isomorphic in the category x [CC,Set,Set] ! 21:21:46 _llll_: (a bit complicated and not terribly important to understand at this stage) 21:22:15 _llll_: ok, so as i was saying 21:22:22 _llll_: if f:A-->B then Ff is a function FA-->FB 21:22:42 _llll_: write a^f for the element Ff(a) 21:22:52 _llll_: ie if a in FA then a^f is in FB 21:23:23 _llll_: the statement "F is a functor CC-->Set" means that if f:A-->B and g:B-->B' and a in FA, then 21:23:32 _llll_: (a^f)^g = a^(f#g) 21:23:40 _llll_: (this is equality in the set F(B')) 21:23:47 _llll_: and also a^{id_A} = a 21:24:15 _llll_: if you know about groups acting on sets (or groups, or similar) then this is exactly the same rules as there 21:25:05 _llll_: ok, so now what does it mean for m to be in CC,Set(CC(A,-),F)? (ie m:C(A,-) --> F natural transofmration) 21:25:28 _llll_: it means that for every B in CC, we have a function m_B : CC(A,B) --> FB 21:26:10 _llll_: such that whenever f:B-->B' (map in CC), m_B # Ff = CC(A,-)(f) # m_{B'} ,----[ a picture of m: C(A,-) --> F posted to pastebin.ca during the seminar] | Theorem (Yoneda Lemma) CC,Set(CC(A,-),F) ~ FA | (an isomorphism of sets natural in F and A) | Proof: | First some notation. | | If f:B-->B' then Ff:FB-->FB' is a map of sets, use the notation Ff(x)=x^f | | So F is a functor iff (x^g)^f = x^{g#f} and x^{id_A}=x | | [e.g., CC(A,-):CC-->Set is the functor with g^f=g#f] | | The m is a natural transformation CC(A,-) to F iff the following squares commute | | g|--------------------------> m_B(g) | - - | | C(A,B) --- m_B -----> FB | | | | | | | | | C(A,f) |Ff | | | | | | | | v v | | | C(A,B') -- m_{B'} --> FB' | | | v | | m_B(g)^f | v | g#f |-------------------------> m_{B'}(g#f) | | I.e., m is natural iff | | m_B(g)^f=m_{B'}(g#f) (*) | | for all g:A-->B and f:B-->B'. | | Put B=A and g=id_A (f:A-->B' is still an arbitrary map from CC). | Then (*) becomes | | m_A(id_A)^f=m_{B'}(f) | | i.e., m is determined by the single element m_A(id_A) in FA. | And conversely, given a in FA, define m:C(A,-)-->F by | | m_B(g)=a^g | | which gives m:C(A,-)-->F natural transformation. | | So the proof is simply to note that | | C(A,-),F --> FA | m |--------> m_A(id_A) | | a^(-) <------|a | | are a pair of mutually inverse bijections. These are natural | in F and A. QED `---- 21:27:31 _llll_: if you unpick what this equation means, starting from g in CC(A,B), the function 'm_B # Ff ' sends this to Ff(m_B(g)) in FB 21:27:40 _llll_: ie to m_B(g)^f 21:27:51 _llll_: using my "action" notation from before 21:28:17 _llll_: and the other side CC(A,-)(f) # m_{B'} sends g to m_{B'}(g#f) 21:28:32 ~carolyn_: ! 21:28:44 _llll_: so m is natural means that m_B(g)^f=m_{B'}(g#f) for all g:A-->B and f:B-->B' (f and g are maps in CC) 21:28:47 _llll_: go ahead carolyn_ 21:29:11 ~carolyn_: what is "commute" in the proof / picture 21:29:21 _llll_: oh, good point 21:29:32 _llll_: it just means that the 2 different ways of going round the diagram are equal 21:29:50 _llll_: so for a square, if you start at the top-left you can either go right then down 21:29:54 _llll_: or down then right 21:30:11 _llll_: both ways give you a composite, and these must be equal 21:30:45 _llll_: so looking at http://pastebin.ca/1071102, the square commutes just means that m(A) # Gf = Ff # m(B) 21:31:12 _llll_: ok, going back to m: CC(A,-) --> F 21:31:24 _llll_: i said that m is natural iff m_B(g)^f=m_{B'}(g#f) for all f,g 21:31:39 _llll_: but now what happens when we put B=A and g=id_A 21:31:49 _llll_: we get m_A(id_A)^f=m_{B'}(f) 21:31:58 _llll_: but this actually determines all of m 21:32:16 _llll_: sice to define m we just need to define m_{B'} for all B' 21:32:29 _llll_: so m is determined by this one element m_A(id_A) in FA 21:32:36 _llll_: conversely, if a is any element in FA 21:33:11 _llll_: define a n_B: CC(A,B) --> FB by n_B(g) := a^g 21:33:20 _llll_: ie n_B(g) = Fg(a) 21:33:37 _llll_: it's not hard to check that n is then a natural transformation CC(A,-) to F 21:33:52 _llll_: ie the bijection between CC(A,-),F and FA 21:34:03 _llll_: sends m to m_A(id_A) 21:34:20 _llll_: and the inverse sends a to this n with n_B(g)=a^g 21:34:50 _llll_: so that pretty much completes the proof, apart from the "natural in A and F" bit, which im going to ignore/leave as an exercise 21:35:03 _llll_: so that was "the yoneda lemma" 21:35:34 _llll_: The next part of the seminar is about adjunctions 21:36:13 _llll_: suppose F:CC-->DD and U:DD-->CC are two functors 21:36:46 _llll_: "F is left adjoint to U" means that there is a bijection between DD(FX,Y) and CC(X,UY) 21:37:05 _llll_: and this has to be "natural in X and Y", which again i wont worry about too much 21:38:02 _llll_: so this means that if f:FX-->Y in DD we get a corresponding f^ : X-->UY in CC 21:38:17 _llll_: and if g:X-->UY in CC then we get a g^: FX-->Y in DD 21:38:26 _llll_: and f^^=f and g^^=g 21:38:58 _llll_: the proof of the yoneda lemma should suggest that everything is determined by what happens when f=id_{FX} and g=id_}{UY} 21:39:40 _llll_: ie id_FX: FX-->FX gets sent to some map unit_{X}:X-->UFX 21:39:58 _llll_: and id_{UY} gets sent to some map counit_Y : FUY --> Y 21:40:43 _llll_: it turns out that these maps actually determine the whole of the adjunction -- that comes from the "natural in X and Y" part, but it's actually just the yoneda lemma proof again 21:40:47 _llll_: namely 21:41:16 _llll_: if f:FX-->Y then f^ is equal to the composite unit_X # F(f) 21:41:33 _llll_: ie X--unit_X--> UFX -- U(f) --> UY 21:41:53 _llll_: and g^ = (FX-- Fg --> FUY -- counit_Y --> Y) 21:42:28 _llll_: the statement that f^^=f then tells us that f is equal to the composite 21:42:58 _llll_: FX --F(unit_X) --> FUFX -- FU(f) ---> FUY -- counit_Y ---> Y 21:43:13 _llll_: ie f= F(unit_X) # FU(f) # counit_Y 21:43:36 _llll_: it turns out that counit is a natural transformation from U#F to the identity 21:43:50 _llll_: ie FU(f) # counit_Y = counit_{FX} # f 21:44:14 _llll_: so "f^^=f" becomes F(unit_X) # counit_{FX} # f = f 21:44:23 _llll_: for all f:FX-->Y 21:44:37 _llll_: so when f=id_FX we get F(unit_X) # counit_{FX} = id_{FX} 21:45:13 _llll_: and similarly, from g:X-->UY and g^^=g we get the equation unit_{UY} # U(counit_Y) = id_{UY} 21:45:30 _llll_: these two equations F(unit_X) # counit_{FX} = id_{FX} and unit_{UY} # U(counit_Y) = id_{UY} are called the "triangle identities" 21:45:49 _llll_: if unit_X and counit_Y are any natural transformations satisfying those, then F and U are adjoint 21:45:59 _llll_: ok, so, why do we care? 21:46:24 _llll_: the main reason is that if F is adjoint to U then it is a theorem that F preserves colimits and U preserves limits 21:47:01 _llll_: one example of an adjunction is that F = free group functor Set --> Group and U=forgetful functor , U:Group-->Set 21:47:29 _llll_: so F preserves colimits 21:47:33 _llll_: and U preserves limits 21:47:50 kommodore: ! 21:47:57 _llll_: go ahead, kommodore 21:48:32 kommodore: Do you really mean F is adjoint to U, or F is left adjoint to U? 21:48:47 _llll_: F is left adjoint to U 21:48:51 _llll_: U is right adjoint to F 21:49:13 kommodore: ok. 21:49:14 _llll_: you can remember because in the bijection DD(FX,Y) ~ CC(X,UY) F is on the left and U is on the right 21:49:31 _llll_: so the result is that left adjoints preserve colimits, and right adjoints preserve limits 21:49:48 _llll_: even for groups, this is perhaps not totally obvious 21:50:33 _llll_: if X is a set, X= coproduct_{x in X} {x} so Free(X) = coproduct_{x in X} F{x} says every free group is a coproduct of infinite cyclic groups 21:50:50 _llll_: so to quickly talk about monads 21:51:01 _llll_: suppsoe F is left adjoint to U in the smeinar I messed up even the definition of T, luckily FunctorSalad put me right. I have therefore made some corrections below -- _llll_ 21:51:11 _llll_: then T=F # U is a functor CC-->CC 21:51:21 _llll_: it sends X to TX=UF(X) 21:51:32 _llll_: i said the adjunction is determined by the unit and counit 21:51:39 _llll_: unit_X : X--> UFX 21:51:45 _llll_: so unit : id --> T 21:51:59 _llll_: (and this is actually a natural transformation from the identity to T) 21:52:13 _llll_: the counit goes conunit_Y:FUY-->Y 21:52:31 _llll_: so therefore U(counit_{FX}) : UFUFX-->UFX 21:52:55 _llll_: ie if we put m_X=U(counit_FX} then m:TTX-->TX 21:53:27 _llll_: and the triangle identities say that m satisfies the equation T(m_X) # m_X = m_{TX} # m_X 21:53:44 _llll_: if we think of the F=free-group / U=forgetful functor stuff 21:54:45 _llll_: then X is a group and TX is the free group on the elements of X 21:54:55 _llll_: so this is like putting the elements of X in boxes 21:55:03 _llll_: which i suppose is why functional programmers like using monads 21:55:49 _llll_: formally, a monad on CC is a functor T:CC-->CC with natural transformations unit_X : id-->T and m: T^2 --> T 21:56:14 _llll_: satisfying T(m_X) # m_X = m_{TX} # m_X and unit_{TX} # m_X = id_X and T(unit_X) # m_X = id_X getting confused elided 21:56:14 FunctorSalad_: ! 21:56:18 _llll_: go ahead FunctorSalad_ 21:56:28 FunctorSalad_: I think for the monad you need to start with a *set* X 21:56:35 FunctorSalad_: the other way would be a comonad 21:58:29 _llll_: so what is TX, it's the set of formal words in elements of X 21:58:40 _llll_: so it's still putting elements of X into boxes 21:59:08 _llll_: ah, yeah this way makes much more sense 21:59:29 _llll_: because an *algebra* for a monad is a map TX--a-->X 21:59:36 _llll_: TX is formal words in elements of X 21:59:53 _llll_: a says how to identify some of these words 22:00:14 _llll_: every group can be given by generators an drelations, and this is actually the same thing 22:00:22 _llll_: ie you can define a category Alg(T) for a monad 22:00:58 _llll_: when the monad comes from an adjunction, if CC is is equivalent to Alg(T) then we say the adjunction is "monadic" 22:01:24 _llll_: this means that the elements of CC (so groups here) are, in some sense, given by genberators and relations using the adjunction 22:01:45 _llll_: there's a theorem called the Beck monadicit theorem that makes this more formal 22:01:58 _llll_: but i think this is a good place to stop 22:02:05 |Steve|: ! 22:02:11 _llll_: time for questions 22:02:14 _llll_: go ahead |Steve| 22:02:23 |Steve|: Alg(T) is the algebra for a monad? What does that mean? 22:02:32 _llll_: Alg(T) is the cateory of algebras for the monad 22:02:46 _llll_: so the objects are TX--a-->X 22:03:47 _llll_: presumably maps a-->b are f: X-->Y such that TX--a-->X-->Y = TX--T(f)-->TY--b-->Y 22:04:41 _llll_: if you can prove that some category is monadic over Set then there are a load of theorems about limits in that category that help you compute things 22:05:00 |Steve|: Is that first diagram TX--a-->X--f-->Y? 22:05:08 _llll_: yeah 22:05:11 |Steve|: Okay, thanks. 22:07:12 _llll_: OK, I guess that ends the seminar 22:10:50 _llll_: Next week somiaj is going to talk about measure theory 22:15:32 ChanServ changed the topic of #mathematics to: For help go to #math | NEXT SEMINAR: Sunday 20th July at 20:00 UTC: Introduction to Measure Theory by somiaj | Later Seminars: see http://freenode-math.com/index.php/Seminars Category:Seminar